(*************************************************************************)
(** Simply-typed Scalina  in Coq.    Regularity                          *)
(** Author: Adriaan Moors, 2008                                          *)
(*************************************************************************)

(** Based on the Coq tutorial at POPL 2008, see
    "Engineering Formal Metatheory", Aydemir, Charguéraud, Pierce,
    Pollack, Weirich. POPL 2008.

    Tutorial authors: Brian Aydemir and Stephanie Weirich, with help
    from Aaron Bohannon, Nate Foster, Benjamin Pierce, Jeffrey
    Vaughan, Dimitrios Vytiniotis, and Steve Zdancewic.  Adapted from
    code by Arthur Charguéraud.
*)

Set Implicit Arguments.
Require Import Metatheory Scalina_Definitions Scalina_Induction Scalina_SubstFresh Scalina_Env support.
Require Import List.


Lemma classifier_of_member_in_lc_tp_is_lc: forall (o: option tp) (mems : list mem) (l : lab) (T : tp),
 lc_tp (tp_struct o mems) -> option_has T (mems ?: l) -> (exists t: tm, lc_tp ({0 ~tp> t}T)).
Proof. 
  intros.

  functional induction (mems_lookup l mems); simpl in H0.
    contradiction.
    subst T. functional induction (mem_getLabel m'). 
     induction o. inversion H. pick_fresh y. forward~ (H3 y). intros Hlcms. inversion Hlcms. inversion H6. exists (fvar y). assumption. 
     exists (fvar y). assumption.

     inversion H. pick_fresh y. forward~ (H1 y). intros Hlcms. inversion Hlcms. inversion H4. exists (fvar y). assumption. 
     exists (fvar y). assumption.
 
     apply IHo0. inversion H. apply lc_struct_noself with (L := L). intros xx xniL. forward~ (H2 xx). intros Hind.
     inversion Hind. auto*.
     apply lc_struct_self with (L := L). assumption. intros xx xniL. forward~ (H4 xx). intros Hind.
     inversion Hind. auto*.
     assumption.
Qed.

Lemma typing_regular : 
 (forall (E : env) (t : tm) (T : tp) (t1 : E |= t ~: T), wf_env E /\ lc_tm t /\ lc_tp T) /\ (*lc_tp T is needed for lc_mem case*)
 (forall (E : env) (T : tp) (w : E |= T ~::Struct), wf_env E /\ lc_tp T) /\
 (forall (E : env) (T : tp) (w : E |= T ~::Concrete), wf_env E /\ lc_tp T) /\
 (forall (E : env) (T : tp) (R: tp) (w : E |= T ~< R), wf_env E /\ lc_tp T /\ lc_tp R) /\
 (forall (E : env) (w : wf_env E), wf_env E) /\
 (forall (E : env) (m : mem) (w : E |= m ~:::wf), wf_env E /\ lc_mem m) /\
 (forall (E : env) (ms : list mem) (w : E |= ms ~:::wfs), wf_env E /\ lc_mems ms).
Proof.
  apply typing_wf_mutual_ind; intros.

  split. assumption. auto*.

  destructs H.
    split. assumption. 
    split. auto*.
    assert (exists t : tm, lc_tp ({0 ~tp> t}T)).
    apply classifier_of_member_in_lc_tp_is_lc with (o := o) (mems := mems) (l := l). assumption. assumption. 
    destruct H1. assumption.

   destructs H.
    split. assumption.
    split. induction e. auto*. 
    induction e. assumption.

  split.
    pick_fresh x. assert (wf_env (E & x ~ SelfTp)). destruct (H x); auto*. apply wf_env_remove2 with (F:=x ~ SelfTp). assumption.
    apply_fresh lc_struct_self as x. assumption. 
    destruct (H x) as [_ Hlcs]. auto*. fold (open_mems ms x). assumption.
  destruct H. split; trivial. inversions* H0. auto*.
  auto*.
  auto*.
  auto*.
  auto*.
  auto*.
  auto*.
  auto*.
Qed.    
(** Wow, I already forgot which case this is supposed to prove, `auto*` seems to do the trick.. :)
    
(* derive wf_env E from wf_env E & x ~ SelfTp for some arbitrary x
 -- do the pick_fresh after the split --> need more generality for right part of the conjunction
*)
    pick_fresh y. forward~ (H y) as K. inversions K. 
    assert (wf_env (E & empty)).  (*TODO: find more elegant way *)
      apply wf_env_remove2 with (F:= y ~ SelfTp). auto*. auto*.


(* prove the lc_tp part *)
    apply lc_struct_self with (L := L). 
      assumption. (* needed to add the hypo `lc_tp SelfTp` to wf_struct_self *)

      intros. 
      forward~ (H x). intros [_ Hlc]. auto. 

   destruct H.  split. assumption. inversions H0. auto.

   destructs H. split. assumption. auto*. 

   split. assumption. auto*.

   split. assumption. auto*. 

   destructs H0. split. assumption. auto*. 
Qed.*)

(** morale: option_has in lc_mem leads to stupid induction principle *)

Lemma value_regular : forall e,
  value e -> lc_tm e.
Proof.
  induction 1; auto*.
Qed.

(*
Lemma rt_lookup_agrees_forAll: forall (f: mem -> Prop) ms l m,
  list_forAll (map f ms) -> f mems_lookup_mem l ms.
Proof.
  intros f ms l m Hall Hlu.
  induction Hlu; simpl in *; auto*.
Qed.*)


Lemma lc_tp_implies_lc_mems_rt_expand: forall (T: tp) (ms: list mem),
  lc_tp T -> rt_expand T ms -> (forall t: tm, lc_tm t -> lc_mems (open_mems ms t)).
Proof.
  intros T ms Hlc Hexp.
  induction Hexp.
  induction o; inversion Hlc. subst. intros.
  unfold open_mems. pick_fresh x. forward~ (H2 x). intros. 
  apply lc_mems_forAll_conv.
  pose (lc_mems_forAll H0).
  rewrite map_map in *.
  
  apply under_forAll_map_retain_in with (f :=  (fun m : mem => lc_mem ({0 ~mem> x}m))) (g := (fun m : mem => lc_mem ({0 ~mem> t}m))).
  intros m Hm_in_ms Hlcmem. 

(*  destructs (lc_open_some_lc_open_any x). auto*.*)
  assert (x \notin fv_mem m) as Hnotinm. assert (x \notin fv_mems ms) as Hx_notin_ms. auto*. unfold fv_mems in Hx_notin_ms.


  pose (notinUnion_forAll_notin ms fv_mem Hx_notin_ms). 

  apply (forAll_implies_forIn ms m (fun m => x \notin fv_mem m) l0). assumption.

  pose (Heq := @subst_intro_mem x m t Hnotinm H).
  
  unfold open_mem in Heq.
  rewrite Heq.
  destructs (subst_lc x H).
  auto*.


  assumption.

(* TODO factor out above part of the proof as lemma to avoid copy/paste*)

 subst. intros.
  unfold open_mems. pick_fresh x. forward~ (H0 x). intros.
  apply lc_mems_forAll_conv.
  pose (lc_mems_forAll H1).
  rewrite map_map in *.
  
 apply under_forAll_map_retain_in with (f :=  (fun m : mem => lc_mem ({0 ~mem> x}m))) (g := (fun m : mem => lc_mem ({0 ~mem> t}m))).
  intros m Hm_in_ms Hlcmem. 

(*  destructs (lc_open_some_lc_open_any x). auto*.*)
  assert (x \notin fv_mem m) as Hnotinm. assert (x \notin fv_mems ms) as Hx_notin_ms. auto*. unfold fv_mems in Hx_notin_ms.



  pose (notinUnion_forAll_notin ms fv_mem Hx_notin_ms). 

  apply (forAll_implies_forIn ms m (fun m => x \notin fv_mem m) l0). assumption.

  pose (Heq := @subst_intro_mem x m t Hnotinm H).
  
  unfold open_mem in Heq.
  rewrite Heq.
  destructs (subst_lc x H).
  auto*.


  assumption.


Qed.

Lemma red_regular : forall e e',
  red e e' -> lc_tm e /\ lc_tm e'.
Proof.
  induction 1. inversion H. inversion H3. split. auto*. 

  pose (l0:= lc_tp_implies_lc_mems_rt_expand H5 H0).
  unfold open_mems in l0. pose (l1:= lc_mems_forAll (l0 (new T) H3)). rewrite map_map in l1. clear l0. 

  clear H0. (*otherwise induction hypothesis becomes too strong*)
  functional induction (mems_lookup l ms).   
    contradiction.
    (* case: found member with right label *)
    clear e0. 
    simpl in H1. functional induction (mem_getRhs m').
    unfold mem_getLabel in *. (*don't perform functional induction, it breaks the proof!*)
    induction o. 
      simpl in H1. subst. simpl in l1. destruct l1 as [Hlcmem _]. inversion Hlcmem. auto*.
      contradiction.

    (*inductive case *)
    simpl in l1. destruct l1 as [_ ForTail]. apply (IHo H1 ForTail).
  
  auto*.
Qed.